Section: Dissemination
Promoting Scientific Activities
Scientific Events Selection
Chair of Conference Program Committees
Yves Bertot is program co-chair, with Viktor Vafeiadis from MPI-SWS in Germany for the ACM conference Certified Programs and Proofs (CPP) to be held in Paris in January 2017. Most of the editorial activities took place in 2016.
Member of the Conference Program Committees
-
Yves Bertot and Laurent Théry were members of the conference program committee for the conference Interactive Theorem Proving (ITP) and User-Interfaces for Theorem Provers (UITP).
-
Cyril Cohen was a member ot the program committee for the 8th Coq workshop.
Reviewer
Cyril Cohen was reviewer for the conferences CSL 2016 and ITP 2016. Laurent Théry was a reviewer for the conferences TACAS'17 and CPP'17. Benjamin Grégoire was a reviewer for TACAS. Benjamin Grégoire was a reviewer for PoPL 2017.
Journal
Reviewer - Reviewing Activities
Cyril Cohen was a reviewer for Journal of Automated Reasoning. Laurent Théry was a reviewer for Journal of Automated Reasoning and Journal of Symbolic Computation. Yves Bertot was a reviewer for Journal of Automated Reasoning and Computational Geometry: Theory and Applications.
Invited Talks
Laurent Théry gave an invited talk at MAP'16 (Mathematics, Algorithms, and Proofs).
Cyril Cohen gave an invited talk at the ELFIC seminar on the Paris-Saclay campus (Elfic stands for Éléments finis formellement vérifiés).
Leadership within the Scientific Community
Yves Bertot and Maxime Dénès have been working on setting up a Consortium of users for the Coq system. The consortium should start in the early days of 2017. Yves Bertot, Enrico Tassi, and Maxime Dénès were invited to the kick-off meeting of the Expedition in Computing entitled “the science of deep specification” funded by the NSF foundation, along with three other developers from the pi.r2 project-team, as expert developers of the Coq system. This kick-off meeting took place in June.